↳ Prolog
↳ PrologToPiTRSProof
rem_in(X, Y, X) → U4(X, Y, notZero_in(Y))
notZero_in(s(X)) → notZero_out(s(X))
U4(X, Y, notZero_out(Y)) → U5(X, Y, geq_in(X, Y))
geq_in(X, 0) → geq_out(X, 0)
geq_in(s(X), s(Y)) → U7(X, Y, geq_in(X, Y))
U7(X, Y, geq_out(X, Y)) → geq_out(s(X), s(Y))
U5(X, Y, geq_out(X, Y)) → rem_out(X, Y, X)
rem_in(X, Y, R) → U1(X, Y, R, notZero_in(Y))
U1(X, Y, R, notZero_out(Y)) → U2(X, Y, R, sub_in(X, Y, Z))
sub_in(X, 0, X) → sub_out(X, 0, X)
sub_in(s(X), s(Y), Z) → U6(X, Y, Z, sub_in(X, Y, Z))
U6(X, Y, Z, sub_out(X, Y, Z)) → sub_out(s(X), s(Y), Z)
U2(X, Y, R, sub_out(X, Y, Z)) → U3(X, Y, R, rem_in(Z, Y, R))
U3(X, Y, R, rem_out(Z, Y, R)) → rem_out(X, Y, R)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
rem_in(X, Y, X) → U4(X, Y, notZero_in(Y))
notZero_in(s(X)) → notZero_out(s(X))
U4(X, Y, notZero_out(Y)) → U5(X, Y, geq_in(X, Y))
geq_in(X, 0) → geq_out(X, 0)
geq_in(s(X), s(Y)) → U7(X, Y, geq_in(X, Y))
U7(X, Y, geq_out(X, Y)) → geq_out(s(X), s(Y))
U5(X, Y, geq_out(X, Y)) → rem_out(X, Y, X)
rem_in(X, Y, R) → U1(X, Y, R, notZero_in(Y))
U1(X, Y, R, notZero_out(Y)) → U2(X, Y, R, sub_in(X, Y, Z))
sub_in(X, 0, X) → sub_out(X, 0, X)
sub_in(s(X), s(Y), Z) → U6(X, Y, Z, sub_in(X, Y, Z))
U6(X, Y, Z, sub_out(X, Y, Z)) → sub_out(s(X), s(Y), Z)
U2(X, Y, R, sub_out(X, Y, Z)) → U3(X, Y, R, rem_in(Z, Y, R))
U3(X, Y, R, rem_out(Z, Y, R)) → rem_out(X, Y, R)
REM_IN(X, Y, X) → U41(X, Y, notZero_in(Y))
REM_IN(X, Y, X) → NOTZERO_IN(Y)
U41(X, Y, notZero_out(Y)) → U51(X, Y, geq_in(X, Y))
U41(X, Y, notZero_out(Y)) → GEQ_IN(X, Y)
GEQ_IN(s(X), s(Y)) → U71(X, Y, geq_in(X, Y))
GEQ_IN(s(X), s(Y)) → GEQ_IN(X, Y)
REM_IN(X, Y, R) → U11(X, Y, R, notZero_in(Y))
REM_IN(X, Y, R) → NOTZERO_IN(Y)
U11(X, Y, R, notZero_out(Y)) → U21(X, Y, R, sub_in(X, Y, Z))
U11(X, Y, R, notZero_out(Y)) → SUB_IN(X, Y, Z)
SUB_IN(s(X), s(Y), Z) → U61(X, Y, Z, sub_in(X, Y, Z))
SUB_IN(s(X), s(Y), Z) → SUB_IN(X, Y, Z)
U21(X, Y, R, sub_out(X, Y, Z)) → U31(X, Y, R, rem_in(Z, Y, R))
U21(X, Y, R, sub_out(X, Y, Z)) → REM_IN(Z, Y, R)
rem_in(X, Y, X) → U4(X, Y, notZero_in(Y))
notZero_in(s(X)) → notZero_out(s(X))
U4(X, Y, notZero_out(Y)) → U5(X, Y, geq_in(X, Y))
geq_in(X, 0) → geq_out(X, 0)
geq_in(s(X), s(Y)) → U7(X, Y, geq_in(X, Y))
U7(X, Y, geq_out(X, Y)) → geq_out(s(X), s(Y))
U5(X, Y, geq_out(X, Y)) → rem_out(X, Y, X)
rem_in(X, Y, R) → U1(X, Y, R, notZero_in(Y))
U1(X, Y, R, notZero_out(Y)) → U2(X, Y, R, sub_in(X, Y, Z))
sub_in(X, 0, X) → sub_out(X, 0, X)
sub_in(s(X), s(Y), Z) → U6(X, Y, Z, sub_in(X, Y, Z))
U6(X, Y, Z, sub_out(X, Y, Z)) → sub_out(s(X), s(Y), Z)
U2(X, Y, R, sub_out(X, Y, Z)) → U3(X, Y, R, rem_in(Z, Y, R))
U3(X, Y, R, rem_out(Z, Y, R)) → rem_out(X, Y, R)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
REM_IN(X, Y, X) → U41(X, Y, notZero_in(Y))
REM_IN(X, Y, X) → NOTZERO_IN(Y)
U41(X, Y, notZero_out(Y)) → U51(X, Y, geq_in(X, Y))
U41(X, Y, notZero_out(Y)) → GEQ_IN(X, Y)
GEQ_IN(s(X), s(Y)) → U71(X, Y, geq_in(X, Y))
GEQ_IN(s(X), s(Y)) → GEQ_IN(X, Y)
REM_IN(X, Y, R) → U11(X, Y, R, notZero_in(Y))
REM_IN(X, Y, R) → NOTZERO_IN(Y)
U11(X, Y, R, notZero_out(Y)) → U21(X, Y, R, sub_in(X, Y, Z))
U11(X, Y, R, notZero_out(Y)) → SUB_IN(X, Y, Z)
SUB_IN(s(X), s(Y), Z) → U61(X, Y, Z, sub_in(X, Y, Z))
SUB_IN(s(X), s(Y), Z) → SUB_IN(X, Y, Z)
U21(X, Y, R, sub_out(X, Y, Z)) → U31(X, Y, R, rem_in(Z, Y, R))
U21(X, Y, R, sub_out(X, Y, Z)) → REM_IN(Z, Y, R)
rem_in(X, Y, X) → U4(X, Y, notZero_in(Y))
notZero_in(s(X)) → notZero_out(s(X))
U4(X, Y, notZero_out(Y)) → U5(X, Y, geq_in(X, Y))
geq_in(X, 0) → geq_out(X, 0)
geq_in(s(X), s(Y)) → U7(X, Y, geq_in(X, Y))
U7(X, Y, geq_out(X, Y)) → geq_out(s(X), s(Y))
U5(X, Y, geq_out(X, Y)) → rem_out(X, Y, X)
rem_in(X, Y, R) → U1(X, Y, R, notZero_in(Y))
U1(X, Y, R, notZero_out(Y)) → U2(X, Y, R, sub_in(X, Y, Z))
sub_in(X, 0, X) → sub_out(X, 0, X)
sub_in(s(X), s(Y), Z) → U6(X, Y, Z, sub_in(X, Y, Z))
U6(X, Y, Z, sub_out(X, Y, Z)) → sub_out(s(X), s(Y), Z)
U2(X, Y, R, sub_out(X, Y, Z)) → U3(X, Y, R, rem_in(Z, Y, R))
U3(X, Y, R, rem_out(Z, Y, R)) → rem_out(X, Y, R)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDP
SUB_IN(s(X), s(Y), Z) → SUB_IN(X, Y, Z)
rem_in(X, Y, X) → U4(X, Y, notZero_in(Y))
notZero_in(s(X)) → notZero_out(s(X))
U4(X, Y, notZero_out(Y)) → U5(X, Y, geq_in(X, Y))
geq_in(X, 0) → geq_out(X, 0)
geq_in(s(X), s(Y)) → U7(X, Y, geq_in(X, Y))
U7(X, Y, geq_out(X, Y)) → geq_out(s(X), s(Y))
U5(X, Y, geq_out(X, Y)) → rem_out(X, Y, X)
rem_in(X, Y, R) → U1(X, Y, R, notZero_in(Y))
U1(X, Y, R, notZero_out(Y)) → U2(X, Y, R, sub_in(X, Y, Z))
sub_in(X, 0, X) → sub_out(X, 0, X)
sub_in(s(X), s(Y), Z) → U6(X, Y, Z, sub_in(X, Y, Z))
U6(X, Y, Z, sub_out(X, Y, Z)) → sub_out(s(X), s(Y), Z)
U2(X, Y, R, sub_out(X, Y, Z)) → U3(X, Y, R, rem_in(Z, Y, R))
U3(X, Y, R, rem_out(Z, Y, R)) → rem_out(X, Y, R)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PiDP
↳ PiDP
SUB_IN(s(X), s(Y), Z) → SUB_IN(X, Y, Z)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ QDPSizeChangeProof
↳ PiDP
↳ PiDP
SUB_IN(s(X), s(Y)) → SUB_IN(X, Y)
From the DPs we obtained the following set of size-change graphs:
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
GEQ_IN(s(X), s(Y)) → GEQ_IN(X, Y)
rem_in(X, Y, X) → U4(X, Y, notZero_in(Y))
notZero_in(s(X)) → notZero_out(s(X))
U4(X, Y, notZero_out(Y)) → U5(X, Y, geq_in(X, Y))
geq_in(X, 0) → geq_out(X, 0)
geq_in(s(X), s(Y)) → U7(X, Y, geq_in(X, Y))
U7(X, Y, geq_out(X, Y)) → geq_out(s(X), s(Y))
U5(X, Y, geq_out(X, Y)) → rem_out(X, Y, X)
rem_in(X, Y, R) → U1(X, Y, R, notZero_in(Y))
U1(X, Y, R, notZero_out(Y)) → U2(X, Y, R, sub_in(X, Y, Z))
sub_in(X, 0, X) → sub_out(X, 0, X)
sub_in(s(X), s(Y), Z) → U6(X, Y, Z, sub_in(X, Y, Z))
U6(X, Y, Z, sub_out(X, Y, Z)) → sub_out(s(X), s(Y), Z)
U2(X, Y, R, sub_out(X, Y, Z)) → U3(X, Y, R, rem_in(Z, Y, R))
U3(X, Y, R, rem_out(Z, Y, R)) → rem_out(X, Y, R)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PiDP
GEQ_IN(s(X), s(Y)) → GEQ_IN(X, Y)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ QDPSizeChangeProof
↳ PiDP
GEQ_IN(s(X), s(Y)) → GEQ_IN(X, Y)
From the DPs we obtained the following set of size-change graphs:
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
U21(X, Y, R, sub_out(X, Y, Z)) → REM_IN(Z, Y, R)
REM_IN(X, Y, R) → U11(X, Y, R, notZero_in(Y))
U11(X, Y, R, notZero_out(Y)) → U21(X, Y, R, sub_in(X, Y, Z))
rem_in(X, Y, X) → U4(X, Y, notZero_in(Y))
notZero_in(s(X)) → notZero_out(s(X))
U4(X, Y, notZero_out(Y)) → U5(X, Y, geq_in(X, Y))
geq_in(X, 0) → geq_out(X, 0)
geq_in(s(X), s(Y)) → U7(X, Y, geq_in(X, Y))
U7(X, Y, geq_out(X, Y)) → geq_out(s(X), s(Y))
U5(X, Y, geq_out(X, Y)) → rem_out(X, Y, X)
rem_in(X, Y, R) → U1(X, Y, R, notZero_in(Y))
U1(X, Y, R, notZero_out(Y)) → U2(X, Y, R, sub_in(X, Y, Z))
sub_in(X, 0, X) → sub_out(X, 0, X)
sub_in(s(X), s(Y), Z) → U6(X, Y, Z, sub_in(X, Y, Z))
U6(X, Y, Z, sub_out(X, Y, Z)) → sub_out(s(X), s(Y), Z)
U2(X, Y, R, sub_out(X, Y, Z)) → U3(X, Y, R, rem_in(Z, Y, R))
U3(X, Y, R, rem_out(Z, Y, R)) → rem_out(X, Y, R)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
U21(X, Y, R, sub_out(X, Y, Z)) → REM_IN(Z, Y, R)
REM_IN(X, Y, R) → U11(X, Y, R, notZero_in(Y))
U11(X, Y, R, notZero_out(Y)) → U21(X, Y, R, sub_in(X, Y, Z))
notZero_in(s(X)) → notZero_out(s(X))
sub_in(X, 0, X) → sub_out(X, 0, X)
sub_in(s(X), s(Y), Z) → U6(X, Y, Z, sub_in(X, Y, Z))
U6(X, Y, Z, sub_out(X, Y, Z)) → sub_out(s(X), s(Y), Z)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
REM_IN(X, Y) → U11(X, Y, notZero_in(Y))
U21(Y, sub_out(Z)) → REM_IN(Z, Y)
U11(X, Y, notZero_out) → U21(Y, sub_in(X, Y))
notZero_in(s(X)) → notZero_out
sub_in(X, 0) → sub_out(X)
sub_in(s(X), s(Y)) → U6(sub_in(X, Y))
U6(sub_out(Z)) → sub_out(Z)
notZero_in(x0)
sub_in(x0, x1)
U6(x0)
REM_IN(y0, s(x0)) → U11(y0, s(x0), notZero_out)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ QDP
↳ UsableRulesProof
REM_IN(y0, s(x0)) → U11(y0, s(x0), notZero_out)
U21(Y, sub_out(Z)) → REM_IN(Z, Y)
U11(X, Y, notZero_out) → U21(Y, sub_in(X, Y))
notZero_in(s(X)) → notZero_out
sub_in(X, 0) → sub_out(X)
sub_in(s(X), s(Y)) → U6(sub_in(X, Y))
U6(sub_out(Z)) → sub_out(Z)
notZero_in(x0)
sub_in(x0, x1)
U6(x0)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
REM_IN(y0, s(x0)) → U11(y0, s(x0), notZero_out)
U21(Y, sub_out(Z)) → REM_IN(Z, Y)
U11(X, Y, notZero_out) → U21(Y, sub_in(X, Y))
sub_in(X, 0) → sub_out(X)
sub_in(s(X), s(Y)) → U6(sub_in(X, Y))
U6(sub_out(Z)) → sub_out(Z)
notZero_in(x0)
sub_in(x0, x1)
U6(x0)
notZero_in(x0)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
REM_IN(y0, s(x0)) → U11(y0, s(x0), notZero_out)
U21(Y, sub_out(Z)) → REM_IN(Z, Y)
U11(X, Y, notZero_out) → U21(Y, sub_in(X, Y))
sub_in(X, 0) → sub_out(X)
sub_in(s(X), s(Y)) → U6(sub_in(X, Y))
U6(sub_out(Z)) → sub_out(Z)
sub_in(x0, x1)
U6(x0)
U11(s(x0), s(x1), notZero_out) → U21(s(x1), U6(sub_in(x0, x1)))
U11(x0, 0, notZero_out) → U21(0, sub_out(x0))
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
REM_IN(y0, s(x0)) → U11(y0, s(x0), notZero_out)
U11(s(x0), s(x1), notZero_out) → U21(s(x1), U6(sub_in(x0, x1)))
U11(x0, 0, notZero_out) → U21(0, sub_out(x0))
U21(Y, sub_out(Z)) → REM_IN(Z, Y)
sub_in(X, 0) → sub_out(X)
sub_in(s(X), s(Y)) → U6(sub_in(X, Y))
U6(sub_out(Z)) → sub_out(Z)
sub_in(x0, x1)
U6(x0)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
REM_IN(y0, s(x0)) → U11(y0, s(x0), notZero_out)
U11(s(x0), s(x1), notZero_out) → U21(s(x1), U6(sub_in(x0, x1)))
U21(Y, sub_out(Z)) → REM_IN(Z, Y)
sub_in(X, 0) → sub_out(X)
sub_in(s(X), s(Y)) → U6(sub_in(X, Y))
U6(sub_out(Z)) → sub_out(Z)
sub_in(x0, x1)
U6(x0)
U21(s(z1), sub_out(x1)) → REM_IN(x1, s(z1))
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ ForwardInstantiation
REM_IN(y0, s(x0)) → U11(y0, s(x0), notZero_out)
U21(s(z1), sub_out(x1)) → REM_IN(x1, s(z1))
U11(s(x0), s(x1), notZero_out) → U21(s(x1), U6(sub_in(x0, x1)))
sub_in(X, 0) → sub_out(X)
sub_in(s(X), s(Y)) → U6(sub_in(X, Y))
U6(sub_out(Z)) → sub_out(Z)
sub_in(x0, x1)
U6(x0)
REM_IN(s(y_0), s(x1)) → U11(s(y_0), s(x1), notZero_out)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
U11(s(x0), s(x1), notZero_out) → U21(s(x1), U6(sub_in(x0, x1)))
U21(s(z1), sub_out(x1)) → REM_IN(x1, s(z1))
REM_IN(s(y_0), s(x1)) → U11(s(y_0), s(x1), notZero_out)
sub_in(X, 0) → sub_out(X)
sub_in(s(X), s(Y)) → U6(sub_in(X, Y))
U6(sub_out(Z)) → sub_out(Z)
sub_in(x0, x1)
U6(x0)
U21(s(x0), sub_out(s(y_0))) → REM_IN(s(y_0), s(x0))
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ QDPOrderProof
U21(s(x0), sub_out(s(y_0))) → REM_IN(s(y_0), s(x0))
U11(s(x0), s(x1), notZero_out) → U21(s(x1), U6(sub_in(x0, x1)))
REM_IN(s(y_0), s(x1)) → U11(s(y_0), s(x1), notZero_out)
sub_in(X, 0) → sub_out(X)
sub_in(s(X), s(Y)) → U6(sub_in(X, Y))
U6(sub_out(Z)) → sub_out(Z)
sub_in(x0, x1)
U6(x0)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
U11(s(x0), s(x1), notZero_out) → U21(s(x1), U6(sub_in(x0, x1)))
Used ordering: Polynomial interpretation [25]:
U21(s(x0), sub_out(s(y_0))) → REM_IN(s(y_0), s(x0))
REM_IN(s(y_0), s(x1)) → U11(s(y_0), s(x1), notZero_out)
POL(0) = 0
POL(REM_IN(x1, x2)) = x1
POL(U11(x1, x2, x3)) = x1
POL(U21(x1, x2)) = x2
POL(U6(x1)) = x1
POL(notZero_out) = 0
POL(s(x1)) = 1 + x1
POL(sub_in(x1, x2)) = x1
POL(sub_out(x1)) = x1
sub_in(s(X), s(Y)) → U6(sub_in(X, Y))
sub_in(X, 0) → sub_out(X)
U6(sub_out(Z)) → sub_out(Z)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
U21(s(x0), sub_out(s(y_0))) → REM_IN(s(y_0), s(x0))
REM_IN(s(y_0), s(x1)) → U11(s(y_0), s(x1), notZero_out)
sub_in(X, 0) → sub_out(X)
sub_in(s(X), s(Y)) → U6(sub_in(X, Y))
U6(sub_out(Z)) → sub_out(Z)
sub_in(x0, x1)
U6(x0)